\begin{tabbing}
R{-}discrete\_compat($A$; $B$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if\= Reffect?($A$)\+\+
\\[0ex]then \=if\= Reffect?($B$)\+\+
\\[0ex]then \=(Reffect{-}x($A$) = Reffect{-}x($B$) $\in$ Id)\+
\\[0ex]$\Rightarrow$ (Reffect{-}discrete($A$) = Reffect{-}discrete($B$) $\in$ $\mathbb{B}$)
\-\-\\[0ex]if\= Rinit?($B$)\+
\\[0ex]then \=(Reffect{-}x($A$) = Rinit{-}x($B$) $\in$ Id)\+
\\[0ex]$\Rightarrow$ (Reffect{-}discrete($A$) = Rinit{-}discrete($B$) $\in$ $\mathbb{B}$)
\-\-\\[0ex]else True
\\[0ex]fi 
\-\-\\[0ex]if\= Rinit?($A$)\+
\\[0ex]then \=if\= Reffect?($B$)\+\+
\\[0ex]then \=(Rinit{-}x($A$) = Reffect{-}x($B$) $\in$ Id)\+
\\[0ex]$\Rightarrow$ (Rinit{-}discrete($A$) = Reffect{-}discrete($B$) $\in$ $\mathbb{B}$)
\-\-\\[0ex]if\= Rinit?($B$)\+
\\[0ex]then \=(Rinit{-}x($A$) = Rinit{-}x($B$) $\in$ Id)\+
\\[0ex]$\Rightarrow$ (Rinit{-}discrete($A$) = Rinit{-}discrete($B$) $\in$ $\mathbb{B}$)
\-\-\\[0ex]else True
\\[0ex]fi 
\-\-\\[0ex]else True
\\[0ex]fi 
\-
\end{tabbing}